Section: New Results

Formal specification of AD

Participant : Laurent Hascoët.

There is very little formal specification of AD as a program transformation, and consequently no formal proof of its correctness. Correctness of tangent AD is problematic: if defined as equivalence of the tangent program semantics with the mathematical derivative of the semantics of the original code, correctness is mostly granted for simple staight-line programs, and in general not granted for programs with control. Therefore formal proofs of correctness appear unreachable at present. Fortunately, there is little concern about the practical relevance of tangent AD. The confidence of end-users regarding tangent AD is justified by everyday experience.

Adjoint-mode AD poses a different challenge. The adjoint AD transformation is by no means simple nor intuitive. Its specification is informal, so that end-users of AD cannot gain a strong confidence in the process. Moreover, the constant quest for efficiency of the adjoint code has introduced a number of improvements and tradeoffs that are defined informally. These improvements make the adjoint code intricate and sometimes interact to cause subtle bugs. On the other hand, the good news is that the difference between the adjoint code and the tangent code only lies in the order of the derivatives computations and not in their nature. A formal proof of semantic equivalence is thus conceivable.

The first step towards such a proof is a formal specification of both tangent-mode and adjoint-mode AD, including the specification of the program static data-flow analyses that the transformations require. We have provided this specification in terms of Data-Flow equations for the analyses, and in terms of Structural Operational Semantics (more precisely Natural Semantics) for the AD transformations themselves [19] . This specification will be the basis for future formal proofs of equivalence between tangent AD and adjoint AD.